/* Benchmarks for the PionterC verifier. */

// list visit

struct list 
{
  int data;
  struct list* next;
};

/*@ n>=0
  @*/
struct list* creatList(int n)
{
  struct list* l;
  struct list* p;
  int i;
  
  p=null;
  l=null;
  i = 0;
  
  while(i<=n) /*@*/ 
  {
    p = alloc(struct list);
    p->next = l;
    l = p;
  }
  p = null;
  return l;
}
/*@ 
  @*/
  